﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;

namespace TruthTree2.PC.Logic
{
    public enum TreeState
    {
        Incomplete,
        Closed,
        Open
    }
    public class Tree
    {


        internal List<Pair<Sentence, bool>> sentences;
        internal Tree parent;
        internal Tree left, right;

        public TreeState State { get; private set; }

        public Tree(List<Sentence> sen)
        {
            sentences = new List<Pair<Sentence, bool>>(sen.Count);
            parent = null;
            left = null;
            right = null;
            State = TreeState.Incomplete;

            sen.Sort();
            foreach (Sentence s in sen)
            {
                sentences.Add(new Pair<Sentence, bool>(s, s.Decomposable));
            }
        }

        private void disseminateDecomposition(Decomposition d)
        {
            if (left == null)
            {
                setDecomposition(d);
                return;
            }

            left.disseminateDecomposition(d);
            if (right != null) { right.disseminateDecomposition(d); }
        }

        private void setDecomposition(Decomposition d)
        {
            if (State != TreeState.Incomplete) { return; }

            left = d.GetLeftTree();
            right = d.GetRightTree();

            if (left == null && right != null) { left = right; right = null; }
            if (left != null && right == null)
            {
                sentences.AddRange(left.sentences);
                sentences.Sort((a, b) => { return a.First.CompareTo(b.First); });
                left = null;
            }

            if (left != null) { left.parent = this; }
            if (right != null) { right.parent = this; }
        }

        private List<Sentence> getUnsatisfiedSentences(bool recur = true)
        {
            List<Sentence> sen = new List<Sentence>();
            if (recur && parent != null)
            {
                sen.AddRange(parent.getUnsatisfiedSentences());
            }

            foreach (Pair<Sentence, bool> p in sentences)
            {
                if (p.Second) { sen.Add(p.First); }
            }

            return sen;
        }

        private List<Sentence> getSentences(bool recur = true)
        {
            List<Sentence> sen = new List<Sentence>();
            if (recur && parent != null)
            {
                sen.AddRange(parent.getSentences());
            }

            foreach (Pair<Sentence, bool> p in sentences)
            {
                sen.Add(p.First);
            }

            return sen;
        }

        private void checkForCompletion()
        {
            if (left != null)
            {
                left.checkForCompletion();

                if (right != null)
                {
                    right.checkForCompletion();

                    if (left.State == TreeState.Open || right.State == TreeState.Open)
                    {
                        State = TreeState.Open;
                    }
                    else if (left.State == TreeState.Closed && right.State == TreeState.Closed)
                    {
                        State = TreeState.Closed;
                    }
                    else
                    {
                        State = TreeState.Incomplete;
                    }
                }
                else
                {
                    State = left.State;
                }

                return;
            }

            List<Sentence> all = getSentences();
            for (int a = 0; a < all.Count; a++)
            {
                for (int b = a + 1; b < all.Count; b++)
                {
                    if (all[a].Equal(all[b].GetNegation()) || all[b].Equal(all[a].GetNegation()))
                    {
                        State = TreeState.Closed;
                        return;
                    }
                }
            }

            List<Sentence> uns = getUnsatisfiedSentences();
            if (uns.Count != 0)
            {
                State = TreeState.Incomplete;
                return;
            }

            State = TreeState.Open;
        }

        public bool Decompose()
        {
            checkForCompletion();
            if (State != TreeState.Incomplete) { return false; }

            foreach (Pair<Sentence, bool> p in sentences)
            {
                if (!p.Second) { continue; }
                disseminateDecomposition(p.First.GetDecomposition());
                p.Second = false;
                return true;
            }

            if (left != null)
            {
                if (left.Decompose()) { return true; }

                if (right != null)
                {
                    return right.Decompose();
                }
            }

            return false;
        }

        public string Stringify(int tabs = 0)
        {
            string res = "";

            foreach (Pair<Sentence, bool> p in sentences)
            {
                for (int a = 0; a < tabs; a++) { res += "\t"; }
                res += p.First.ToString() + "\n";
            }

            if (left != null)
            {
                res += left.Stringify(tabs + 1);

                if (right != null)
                {
                    for (int a = 0; a < tabs; a++) { res += "\t"; }
                    res += "\t--\n";
                    res += right.Stringify(tabs + 1);
                }
            }

            return res;
        }
    }
}
